(set-logic QF_BV)
(declare-fun _substvar_7440_ () Bool)
(declare-fun _substvar_7483_ () Bool)
(declare-fun _substvar_9640_ () Bool)
(declare-fun _substvar_10665_ () Bool)
(declare-fun _substvar_11195_ () Bool)
(declare-fun _substvar_11201_ () Bool)
(declare-fun _substvar_11204_ () Bool)
(declare-fun _substvar_11234_ () Bool)
(declare-fun _substvar_11244_ () Bool)
(declare-fun _substvar_11247_ () Bool)
(declare-fun _substvar_11250_ () Bool)
(declare-fun _substvar_11252_ () Bool)
(declare-fun _substvar_11260_ () Bool)
(declare-fun _substvar_11263_ () Bool)
(declare-fun _substvar_11279_ () Bool)
(declare-fun _substvar_11487_ () Bool)
(declare-fun _substvar_11494_ () Bool)
(declare-fun _substvar_11657_ () (_ BitVec 1))
(declare-fun _substvar_11793_ () Bool)
(declare-fun _substvar_11801_ () Bool)
(declare-fun _substvar_11804_ () Bool)
(declare-fun _substvar_11809_ () Bool)
(declare-fun _substvar_11810_ () Bool)
(declare-fun _substvar_11909_ () Bool)
(declare-fun _substvar_11968_ () Bool)
(declare-fun _substvar_12070_ () Bool)
(declare-fun _substvar_12204_ () Bool)
(declare-fun _substvar_12251_ () Bool)
(declare-fun _substvar_12378_ () (_ BitVec 1))
(declare-fun _substvar_12486_ () Bool)
(declare-fun _substvar_12667_ () Bool)
(declare-fun _substvar_12799_ () (_ BitVec 1))
(declare-fun _substvar_12800_ () Bool)
(declare-fun _substvar_12828_ () Bool)
(declare-fun _substvar_12850_ () Bool)
(declare-fun |Scoreboard_is#2823| () Bool)
(declare-fun |Scoreboard#7#2826| () Bool)
(declare-fun |$paramod/FF/WIDTH=1#0#2831| () Bool)
(declare-fun |$paramod/FF/WIDTH=1#1#2833| () (_ BitVec 1))
(declare-fun |$paramod/FF/WIDTH=1#3#2839| () Bool)
(declare-fun |$paramod/MagicPacketTracker/DEPTH=8#1#2844| () Bool)
(declare-fun |Scoreboard#17#2864| () Bool)
(declare-fun |Scoreboard#21#2867| () Bool)
(declare-fun |$paramod/FIFO/WIDTH=8/DEPTH=8_is#2881| () Bool)
(declare-fun |Scoreboard#5#2906| () Bool)
(declare-fun |Scoreboard#6#2910| () Bool)
(define-fun |$paramod/MagicPacketTracker/DEPTH=8_h#2922| () Bool (and _substvar_11909_ |$paramod/MagicPacketTracker/DEPTH=8#1#2844|))
(assert (and _substvar_12667_ (= (= (ite |Scoreboard#7#2826| #b1 #b0) #b1) |$paramod/FF/WIDTH=1#0#2831|) (= |Scoreboard#7#2826| (= |$paramod/FF/WIDTH=1#1#2833| #b1)) _substvar_11793_ _substvar_11801_ _substvar_11804_ _substvar_11809_ _substvar_11810_ _substvar_12204_ (= |Scoreboard_is#2823| |$paramod/FIFO/WIDTH=8/DEPTH=8_is#2881|) _substvar_12070_ |Scoreboard#5#2906| |Scoreboard#6#2910| |Scoreboard#17#2864| _substvar_12850_ |Scoreboard#21#2867| _substvar_7440_ |$paramod/MagicPacketTracker/DEPTH=8_h#2922| _substvar_7483_))
(declare-fun |$paramod/FF/WIDTH=1#1#3186| () (_ BitVec 1))
(declare-fun |Scoreboard#21#3220| () Bool)
(assert (and _substvar_12828_ _substvar_9640_ (= |$paramod/FF/WIDTH=1#1#3186| #b1) _substvar_11968_ _substvar_11195_ _substvar_11201_ _substvar_11204_ _substvar_12486_ (= |Scoreboard#21#3220| _substvar_11279_) _substvar_11234_ _substvar_11244_ _substvar_11247_ _substvar_11252_ _substvar_11263_ _substvar_11487_ _substvar_11494_ _substvar_12251_ _substvar_10665_))
(assert (and (= (ite |$paramod/FF/WIDTH=1#3#2839| (ite |$paramod/FF/WIDTH=1#0#2831| #b1 #b0) |$paramod/FF/WIDTH=1#1#2833|) |$paramod/FF/WIDTH=1#1#3186|) _substvar_11250_ _substvar_11260_))
(assert (and _substvar_12800_ (= (bvand (bvand _substvar_12799_ _substvar_12378_) _substvar_11657_) #b1)))
(check-sat)
(exit)
